The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^5).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^5).


The TRS R consists of the following rules:

f_0(x) → a
f_1(x) → g_1(x, x)
g_1(s(x), y) → b(f_0(y), g_1(x, y))
f_2(x) → g_2(x, x)
g_2(s(x), y) → b(f_1(y), g_2(x, y))
f_3(x) → g_3(x, x)
g_3(s(x), y) → b(f_2(y), g_3(x, y))
f_4(x) → g_4(x, x)
g_4(s(x), y) → b(f_3(y), g_4(x, y))
f_5(x) → g_5(x, x)
g_5(s(x), y) → b(f_4(y), g_5(x, y))

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^5).


The TRS R consists of the following rules:

f_0(x) → a [1]
f_1(x) → g_1(x, x) [1]
g_1(s(x), y) → b(f_0(y), g_1(x, y)) [1]
f_2(x) → g_2(x, x) [1]
g_2(s(x), y) → b(f_1(y), g_2(x, y)) [1]
f_3(x) → g_3(x, x) [1]
g_3(s(x), y) → b(f_2(y), g_3(x, y)) [1]
f_4(x) → g_4(x, x) [1]
g_4(s(x), y) → b(f_3(y), g_4(x, y)) [1]
f_5(x) → g_5(x, x) [1]
g_5(s(x), y) → b(f_4(y), g_5(x, y)) [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

f_0(x) → a [1]
f_1(x) → g_1(x, x) [1]
g_1(s(x), y) → b(f_0(y), g_1(x, y)) [1]
f_2(x) → g_2(x, x) [1]
g_2(s(x), y) → b(f_1(y), g_2(x, y)) [1]
f_3(x) → g_3(x, x) [1]
g_3(s(x), y) → b(f_2(y), g_3(x, y)) [1]
f_4(x) → g_4(x, x) [1]
g_4(s(x), y) → b(f_3(y), g_4(x, y)) [1]
f_5(x) → g_5(x, x) [1]
g_5(s(x), y) → b(f_4(y), g_5(x, y)) [1]

The TRS has the following type information:

f_0 :: s → a:b a :: a:b f_1 :: s → a:b g_1 :: s → s → a:b s :: s → s b :: a:b → a:b → a:b f_2 :: s → a:b g_2 :: s → s → a:b f_3 :: s → a:b g_3 :: s → s → a:b f_4 :: s → a:b g_4 :: s → s → a:b f_5 :: s → a:b g_5 :: s → s → a:b

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

g_1(v0, v1) → null_g_1 [0]
g_2(v0, v1) → null_g_2 [0]
g_3(v0, v1) → null_g_3 [0]
g_4(v0, v1) → null_g_4 [0]
g_5(v0, v1) → null_g_5 [0]

And the following fresh constants:

null_g_1, null_g_2, null_g_3, null_g_4, null_g_5, const

(6) Obligation:

Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: f_0(x) → a [1] f_1(x) → g_1(x, x) [1] g_1(s(x), y) → b(f_0(y), g_1(x, y)) [1] f_2(x) → g_2(x, x) [1] g_2(s(x), y) → b(f_1(y), g_2(x, y)) [1] f_3(x) → g_3(x, x) [1] g_3(s(x), y) → b(f_2(y), g_3(x, y)) [1] f_4(x) → g_4(x, x) [1] g_4(s(x), y) → b(f_3(y), g_4(x, y)) [1] f_5(x) → g_5(x, x) [1] g_5(s(x), y) → b(f_4(y), g_5(x, y)) [1] g_1(v0, v1) → null_g_1 [0] g_2(v0, v1) → null_g_2 [0] g_3(v0, v1) → null_g_3 [0] g_4(v0, v1) → null_g_4 [0] g_5(v0, v1) → null_g_5 [0] The TRS has the following type information: f_0 :: s → a:b:null_g_1:null_g_2:null_g_3:null_g_4:null_g_5 a :: a:b:null_g_1:null_g_2:null_g_3:null_g_4:null_g_5 f_1 :: s → a:b:null_g_1:null_g_2:null_g_3:null_g_4:null_g_5 g_1 :: s → s → a:b:null_g_1:null_g_2:null_g_3:null_g_4:null_g_5 s :: s → s b :: a:b:null_g_1:null_g_2:null_g_3:null_g_4:null_g_5 → a:b:null_g_1:null_g_2:null_g_3:null_g_4:null_g_5 → a:b:null_g_1:null_g_2:null_g_3:null_g_4:null_g_5 f_2 :: s → a:b:null_g_1:null_g_2:null_g_3:null_g_4:null_g_5 g_2 :: s → s → a:b:null_g_1:null_g_2:null_g_3:null_g_4:null_g_5 f_3 :: s → a:b:null_g_1:null_g_2:null_g_3:null_g_4:null_g_5 g_3 :: s → s → a:b:null_g_1:null_g_2:null_g_3:null_g_4:null_g_5 f_4 :: s → a:b:null_g_1:null_g_2:null_g_3:null_g_4:null_g_5 g_4 :: s → s → a:b:null_g_1:null_g_2:null_g_3:null_g_4:null_g_5 f_5 :: s → a:b:null_g_1:null_g_2:null_g_3:null_g_4:null_g_5 g_5 :: s → s → a:b:null_g_1:null_g_2:null_g_3:null_g_4:null_g_5 null_g_1 :: a:b:null_g_1:null_g_2:null_g_3:null_g_4:null_g_5 null_g_2 :: a:b:null_g_1:null_g_2:null_g_3:null_g_4:null_g_5 null_g_3 :: a:b:null_g_1:null_g_2:null_g_3:null_g_4:null_g_5 null_g_4 :: a:b:null_g_1:null_g_2:null_g_3:null_g_4:null_g_5 null_g_5 :: a:b:null_g_1:null_g_2:null_g_3:null_g_4:null_g_5 const :: s Rewrite Strategy: INNERMOST

(7) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

a => 0
null_g_1 => 0
null_g_2 => 0
null_g_3 => 0
null_g_4 => 0
null_g_5 => 0
const => 0

(8) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: x >= 0, z = x
f_1(z) -{ 1 }→ g_1(x, x) :|: x >= 0, z = x
f_2(z) -{ 1 }→ g_2(x, x) :|: x >= 0, z = x
f_3(z) -{ 1 }→ g_3(x, x) :|: x >= 0, z = x
f_4(z) -{ 1 }→ g_4(x, x) :|: x >= 0, z = x
f_5(z) -{ 1 }→ g_5(x, x) :|: x >= 0, z = x
g_1(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
g_1(z, z') -{ 1 }→ 1 + f_0(y) + g_1(x, y) :|: x >= 0, y >= 0, z = 1 + x, z' = y
g_2(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
g_2(z, z') -{ 1 }→ 1 + f_1(y) + g_2(x, y) :|: x >= 0, y >= 0, z = 1 + x, z' = y
g_3(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
g_3(z, z') -{ 1 }→ 1 + f_2(y) + g_3(x, y) :|: x >= 0, y >= 0, z = 1 + x, z' = y
g_4(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
g_4(z, z') -{ 1 }→ 1 + f_3(y) + g_4(x, y) :|: x >= 0, y >= 0, z = 1 + x, z' = y
g_5(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
g_5(z, z') -{ 1 }→ 1 + f_4(y) + g_5(x, y) :|: x >= 0, y >= 0, z = 1 + x, z' = y

Only complete derivations are relevant for the runtime complexity.

(9) CompleteCoflocoProof (EQUIVALENT transformation)

Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V, V3),0,[fun(V, Out)],[V >= 0]). eq(start(V, V3),0,[fun1(V, Out)],[V >= 0]). eq(start(V, V3),0,[fun2(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3),0,[fun3(V, Out)],[V >= 0]). eq(start(V, V3),0,[fun4(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3),0,[fun5(V, Out)],[V >= 0]). eq(start(V, V3),0,[fun6(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3),0,[fun7(V, Out)],[V >= 0]). eq(start(V, V3),0,[fun8(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3),0,[fun9(V, Out)],[V >= 0]). eq(start(V, V3),0,[fun10(V, V3, Out)],[V >= 0,V3 >= 0]). eq(fun(V, Out),1,[],[Out = 0,V1 >= 0,V = V1]). eq(fun1(V, Out),1,[fun2(V2, V2, Ret)],[Out = Ret,V2 >= 0,V = V2]). eq(fun2(V, V3, Out),1,[fun(V4, Ret01),fun2(V5, V4, Ret1)],[Out = 1 + Ret01 + Ret1,V5 >= 0,V4 >= 0,V = 1 + V5,V3 = V4]). eq(fun3(V, Out),1,[fun4(V6, V6, Ret2)],[Out = Ret2,V6 >= 0,V = V6]). eq(fun4(V, V3, Out),1,[fun1(V7, Ret011),fun4(V8, V7, Ret11)],[Out = 1 + Ret011 + Ret11,V8 >= 0,V7 >= 0,V = 1 + V8,V3 = V7]). eq(fun5(V, Out),1,[fun6(V9, V9, Ret3)],[Out = Ret3,V9 >= 0,V = V9]). eq(fun6(V, V3, Out),1,[fun3(V10, Ret012),fun6(V11, V10, Ret12)],[Out = 1 + Ret012 + Ret12,V11 >= 0,V10 >= 0,V = 1 + V11,V3 = V10]). eq(fun7(V, Out),1,[fun8(V12, V12, Ret4)],[Out = Ret4,V12 >= 0,V = V12]). eq(fun8(V, V3, Out),1,[fun5(V13, Ret013),fun8(V14, V13, Ret13)],[Out = 1 + Ret013 + Ret13,V14 >= 0,V13 >= 0,V = 1 + V14,V3 = V13]). eq(fun9(V, Out),1,[fun10(V15, V15, Ret5)],[Out = Ret5,V15 >= 0,V = V15]). eq(fun10(V, V3, Out),1,[fun7(V16, Ret014),fun10(V17, V16, Ret14)],[Out = 1 + Ret014 + Ret14,V17 >= 0,V16 >= 0,V = 1 + V17,V3 = V16]). eq(fun2(V, V3, Out),0,[],[Out = 0,V18 >= 0,V19 >= 0,V = V18,V3 = V19]). eq(fun4(V, V3, Out),0,[],[Out = 0,V20 >= 0,V21 >= 0,V = V20,V3 = V21]). eq(fun6(V, V3, Out),0,[],[Out = 0,V22 >= 0,V23 >= 0,V = V22,V3 = V23]). eq(fun8(V, V3, Out),0,[],[Out = 0,V24 >= 0,V25 >= 0,V = V24,V3 = V25]). eq(fun10(V, V3, Out),0,[],[Out = 0,V26 >= 0,V27 >= 0,V = V26,V3 = V27]). input_output_vars(fun(V,Out),[V],[Out]). input_output_vars(fun1(V,Out),[V],[Out]). input_output_vars(fun2(V,V3,Out),[V,V3],[Out]). input_output_vars(fun3(V,Out),[V],[Out]). input_output_vars(fun4(V,V3,Out),[V,V3],[Out]). input_output_vars(fun5(V,Out),[V],[Out]). input_output_vars(fun6(V,V3,Out),[V,V3],[Out]). input_output_vars(fun7(V,Out),[V],[Out]). input_output_vars(fun8(V,V3,Out),[V,V3],[Out]). input_output_vars(fun9(V,Out),[V],[Out]). input_output_vars(fun10(V,V3,Out),[V,V3],[Out]).

CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components
0. non_recursive : [fun/2]
1. recursive : [fun2/3]
2. non_recursive : [fun1/2]
3. recursive : [fun4/3]
4. non_recursive : [fun3/2]
5. recursive : [fun6/3]
6. non_recursive : [fun5/2]
7. recursive : [fun8/3]
8. non_recursive : [fun7/2]
9. recursive : [fun10/3]
10. non_recursive : [fun9/2]
11. non_recursive : [start/2]

#### Obtained direct recursion through partial evaluation
0. SCC is completely evaluated into other SCCs
1. SCC is partially evaluated into fun2/3
2. SCC is completely evaluated into other SCCs
3. SCC is partially evaluated into fun4/3
4. SCC is completely evaluated into other SCCs
5. SCC is partially evaluated into fun6/3
6. SCC is completely evaluated into other SCCs
7. SCC is partially evaluated into fun8/3
8. SCC is completely evaluated into other SCCs
9. SCC is partially evaluated into fun10/3
10. SCC is completely evaluated into other SCCs
11. SCC is partially evaluated into start/2

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations fun2/3
* CE 14 is refined into CE [23]
* CE 13 is refined into CE [24]


### Cost equations --> "Loop" of fun2/3
* CEs [24] --> Loop 12
* CEs [23] --> Loop 13

### Ranking functions of CR fun2(V,V3,Out)
* RF of phase [12]: [V]

#### Partial ranking functions of CR fun2(V,V3,Out)
* Partial RF of phase [12]:
- RF of loop [12:1]:
V


### Specialization of cost equations fun4/3
* CE 16 is refined into CE [25]
* CE 15 is refined into CE [26,27]


### Cost equations --> "Loop" of fun4/3
* CEs [27] --> Loop 14
* CEs [26] --> Loop 15
* CEs [25] --> Loop 16

### Ranking functions of CR fun4(V,V3,Out)
* RF of phase [14,15]: [V]

#### Partial ranking functions of CR fun4(V,V3,Out)
* Partial RF of phase [14,15]:
- RF of loop [14:1,15:1]:
V


### Specialization of cost equations fun6/3
* CE 18 is refined into CE [28]
* CE 17 is refined into CE [29,30]


### Cost equations --> "Loop" of fun6/3
* CEs [30] --> Loop 17
* CEs [29] --> Loop 18
* CEs [28] --> Loop 19

### Ranking functions of CR fun6(V,V3,Out)
* RF of phase [17,18]: [V]

#### Partial ranking functions of CR fun6(V,V3,Out)
* Partial RF of phase [17,18]:
- RF of loop [17:1,18:1]:
V


### Specialization of cost equations fun8/3
* CE 20 is refined into CE [31]
* CE 19 is refined into CE [32,33]


### Cost equations --> "Loop" of fun8/3
* CEs [33] --> Loop 20
* CEs [32] --> Loop 21
* CEs [31] --> Loop 22

### Ranking functions of CR fun8(V,V3,Out)
* RF of phase [20,21]: [V]

#### Partial ranking functions of CR fun8(V,V3,Out)
* Partial RF of phase [20,21]:
- RF of loop [20:1,21:1]:
V


### Specialization of cost equations fun10/3
* CE 22 is refined into CE [34]
* CE 21 is refined into CE [35,36]


### Cost equations --> "Loop" of fun10/3
* CEs [36] --> Loop 23
* CEs [35] --> Loop 24
* CEs [34] --> Loop 25

### Ranking functions of CR fun10(V,V3,Out)
* RF of phase [23,24]: [V]

#### Partial ranking functions of CR fun10(V,V3,Out)
* Partial RF of phase [23,24]:
- RF of loop [23:1,24:1]:
V


### Specialization of cost equations start/2
* CE 2 is refined into CE [37]
* CE 3 is refined into CE [38,39]
* CE 4 is refined into CE [40,41]
* CE 5 is refined into CE [42,43]
* CE 6 is refined into CE [44,45]
* CE 7 is refined into CE [46,47]
* CE 8 is refined into CE [48,49]
* CE 9 is refined into CE [50,51]
* CE 10 is refined into CE [52,53]
* CE 11 is refined into CE [54,55]
* CE 12 is refined into CE [56,57]


### Cost equations --> "Loop" of start/2
* CEs [37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57] --> Loop 26

### Ranking functions of CR start(V,V3)

#### Partial ranking functions of CR start(V,V3)


Computing Bounds
=====================================

#### Cost of chains of fun2(V,V3,Out):
* Chain [[12],13]: 2*it(12)+0
Such that:it(12) =< Out

with precondition: [V3>=0,Out>=1,V>=Out]

* Chain [13]: 0
with precondition: [Out=0,V>=0,V3>=0]


#### Cost of chains of fun4(V,V3,Out):
* Chain [[14,15],16]: 4*it(14)+2*s(3)+0
Such that:aux(1) =< V3
aux(4) =< V
it(14) =< aux(4)
s(3) =< it(14)*aux(1)

with precondition: [V>=1,V3>=0,Out>=1]

* Chain [16]: 0
with precondition: [Out=0,V>=0,V3>=0]


#### Cost of chains of fun6(V,V3,Out):
* Chain [[17,18],19]: 4*it(17)+4*s(11)+2*s(12)+0
Such that:s(8) =< V3
aux(9) =< V
it(17) =< aux(9)
aux(6) =< s(8)
s(13) =< it(17)*aux(6)
s(11) =< s(13)
s(12) =< s(11)*s(8)

with precondition: [V>=1,V3>=0,Out>=1]

* Chain [19]: 0
with precondition: [Out=0,V>=0,V3>=0]


#### Cost of chains of fun8(V,V3,Out):
* Chain [[20,21],22]: 4*it(20)+4*s(27)+4*s(28)+2*s(29)+0
Such that:s(21) =< V3
aux(14) =< V
it(20) =< aux(14)
aux(11) =< s(21)
s(31) =< it(20)*aux(11)
s(27) =< s(31)
s(30) =< s(27)*aux(11)
s(28) =< s(30)
s(29) =< s(28)*s(21)

with precondition: [V>=1,V3>=0,Out>=1]

* Chain [22]: 0
with precondition: [Out=0,V>=0,V3>=0]


#### Cost of chains of fun10(V,V3,Out):
* Chain [[23,24],25]: 4*it(23)+4*s(49)+4*s(50)+4*s(51)+2*s(52)+0
Such that:s(41) =< V3
aux(19) =< V
it(23) =< aux(19)
aux(16) =< s(41)
s(55) =< it(23)*aux(16)
s(49) =< s(55)
s(54) =< s(49)*aux(16)
s(50) =< s(54)
s(53) =< s(50)*aux(16)
s(51) =< s(53)
s(52) =< s(51)*s(41)

with precondition: [V>=1,V3>=0,Out>=1]

* Chain [25]: 0
with precondition: [Out=0,V>=0,V3>=0]


#### Cost of chains of start(V,V3):
* Chain [26]: 36*s(56)+2*s(61)+2*s(65)+12*s(71)+2*s(72)+12*s(78)+2*s(79)+8*s(87)+2*s(88)+8*s(96)+2*s(97)+4*s(107)+2*s(108)+4*s(118)+2*s(119)+1
Such that:aux(24) =< V
aux(25) =< V3
s(56) =< aux(24)
s(61) =< s(56)*aux(24)
s(69) =< aux(24)
s(70) =< s(56)*s(69)
s(71) =< s(70)
s(72) =< s(71)*aux(24)
s(86) =< s(71)*s(69)
s(87) =< s(86)
s(88) =< s(87)*aux(24)
s(106) =< s(87)*s(69)
s(107) =< s(106)
s(108) =< s(107)*aux(24)
s(65) =< s(56)*aux(25)
s(76) =< aux(25)
s(77) =< s(56)*s(76)
s(78) =< s(77)
s(79) =< s(78)*aux(25)
s(95) =< s(78)*s(76)
s(96) =< s(95)
s(97) =< s(96)*aux(25)
s(117) =< s(96)*s(76)
s(118) =< s(117)
s(119) =< s(118)*aux(25)

with precondition: [V>=0]


Closed-form bounds of start(V,V3):
-------------------------------------
* Chain [26] with precondition: [V>=0]
- Upper bound: 36*V+1+14*V*V+10*V*V*V+6*V*V*V*V+2*V*V*V*V*V+nat(V3)*14*V+nat(V3)*10*nat(V3)*V+nat(V3)*6*nat(V3)*nat(V3)*V+nat(V3)*2*nat(V3)*nat(V3)*nat(V3)*V
- Complexity: n^5

### Maximum cost of start(V,V3): 36*V+1+14*V*V+10*V*V*V+6*V*V*V*V+2*V*V*V*V*V+nat(V3)*14*V+nat(V3)*10*nat(V3)*V+nat(V3)*6*nat(V3)*nat(V3)*V+nat(V3)*2*nat(V3)*nat(V3)*nat(V3)*V
Asymptotic class: n^5
* Total analysis performed in 365 ms.

(10) BOUNDS(1, n^5)